\section{A Distributed Service Scenario}\label{sec:exam}
%\newpage
As an example, let us 
consider a simple scenario of distributed, interacting services (a client $C$ and a service $S$), conveniently represented as located processes:
$$
\mathsf{Sys} \triangleq \component{l_{1}}{0}{}{C} \parallel \bigcomponent{l_2}{0}{}{\component{r}{0}{}{S} \parallel R} \quad\text{where:}\vspace{-3mm}
$$
% We define $C$ and $S$ as follows:
\begin{eqnarray*}
C \!\!& \!\!\triangleq \!\!& \nopen{a}{c:\overline{\sigma}}.\outC{c}{u,p}.\branch{c}{n_1{:}Q_1 \parallel n_1{:}Q_2}.\close{c} \\
S \!\!& \!\!\triangleq \!\!& \nopen{a}{s:\sigma}.\inC{s}{u,p}.\select{s}{n_1.P_1}.\close{s} 
\end{eqnarray*}
and where $R$ represents the platform in which $S$ is deployed.
$\mathsf{Sys}$ may proceed by establishing a session of type $\sigma$ between $S$ and $C$
(realized by $P_1$ and $Q_1$).
Suppose that $R$ stands for an adaptation routine for $S$, defined as an update process:
$$
R \triangleq \mupdate{r}{\component{r_1}{0}{}{S'}  \parallel \component{r_2}{0}{}{T} }{\sigma}{\Delta} \quad\text{where:}\vspace{-3mm}
$$
\begin{eqnarray*}
S' \!\!& \!\!\triangleq \!\!&\!\!\nopen{a}{s:\sigma}.\nopen{b}{d:!(\sigma)}.\throw{d}{s}.\close{d} \\
T \!\!& \!\!\triangleq \!\!& \!\!\nopen{b}{e:?(\sigma)}.\catch{e}{s}.\inC{s}{u,p}.\select{s}{n_1.P_1}.\close{s}.\close{e} 
\end{eqnarray*}
%represents a simple adaptation routine enforcing explicit distribution of interacting processes.
Because $R$ declares no process variables,
it formalizes an update operation which \emph{discards} the behavior located at $r$. We have:
$$
\mathsf{Sys} \pired \component{l_{1}}{0}{}{C} \parallel \bigcomponent{l_2}{0}{}{\component{r_1}{0}{}{S'}  \parallel \component{r_2}{0}{}{T}} 
$$
Thus, 
an update action on $r$
reconfigures the distributed structure of $S$:
in a single step, 
the monolithic service $S$ is replaced by a more flexible 
implementation in which $S'$ (located at $r_1$) first establishes a session with $C$ and then delegates it to $T$ (located at $r_2$).
This update action is transparent to $C$; it 
%Note that the above update % synchronization on $r$ 
is possible because
the interface of $S$ (i.e., $\sigma$)  coincides with the annotation of $R$.
Also, observe that interface $\Delta$ contains entries for session types $!(\sigma)$ and $?(\sigma)$,
which are declared in $S'$ and $T$, resp.

This example can be easily extended with infinite behavior 
(e.g., with $S$ and $R$ as persistent services) 
and with multiple clients. % $C_1, \ldots, C_k$. 
The above scenario already illustrates how
our framework extends the expressiveness of session-typed languages
with located and update processes. % and update actions.
Our type system not only ensures correct communications between $C$ and $S$:
by relying on Cor.~\ref{cor:cons}, we know that well-typedness implies
session consistency, i.e., % between $C$ and $S$, i.e., 
an update action on  $r$ will not occur if $C$ and $S$ have already initiated a session.

%\subsection{More interesting server}
%
%
%We consider the interaction between a Client and a Server as the process $S \parallel C$. 
%The behavior of the server is encoded trough an adaptable process that recursively establishes new sessions with clients:
%$$ S ::= \component{s}{0}{\Delta}{\rec{X:\emptyset, \Delta}{(\open{c:\rho}.c(x).\close{c} \parallel X)} }$$ 
%where $\Delta= \emptyset \shortmid \{\rho\}$ and $\rho = ?(int).\epsilon$.
%
%Clients, in order to connect to the server, must implement a session that is the dual of the one described above: 
%$$C ::= \open{c:\overline{\rho}}.\outC{c}{e}.\close{c}$$
%where $e$ is an expression that evaluates to  $int$.
%
%We now extend this scenario introducing a way of updating the server: $S \parallel C \parallel U$. Here, the update $U$ is meant to extend  the capabilities (for instance by enhancing its performance) of the server by adding an auxiliary machine $M$. The server is then delegating its sessions to $M$:
%$$
%\begin{array}{ll}
%U ::= & \updated{s}{X}{\Delta}{\Delta}{(\component{s}{0}{\Delta}{\rec{X:\emptyset, \Delta}{(\open{c:\rho}.\\
%& \qquad \qquad \open{d:\sigma}.\throw{d}{c}.\close{d}} \parallel X)} \parallel M)}\\
%M ::= &\component{m}{0}{\Delta'}{\rec{X:\emptyset, \Delta'}{(\open{d:\overline{\sigma}}.\catch{d}{e}.\\
%&  \qquad \qquad e(x).\close{e}.\close{d} \parallel X)}}
%\end{array}
% $$
%where $\Delta' = \emptyset \shortmid \ \{\overline{\sigma}\}$ and $\sigma = !(\rho).\epsilon$.




  

%T = open 